/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.File;
import java.util.*;

import common.*;
import jdd.bdd.BDD;

public class Device extends Box {
    /**
     * 
     */
    private static final long serialVersionUID = -6572430105054945928L;
    static boolean has_v6;
    static boolean only_v6;

    // acl name to its id in acllib
    ArrayList<ForwardingRule> fws;
    ArrayList<ForwardingRule6> fws6;
    HashMap <String, Integer> fwbdds;
    HashMap<String, FWDAPSet> fwaps;
    HashMap <String, Integer> fwbdds6;
    MPLSTable mpls_table;
    IPinIP ip_in_ip;

    static FWDAPSet mpls_ap_pkts;
    static FWDAPSet nonmpls_ap_pkts;

    public static FWDAPSet separateMPLS(FWDAPSet in_pkts)
    {
        FWDAPSet outs = new FWDAPSet(in_pkts);
        outs.intersect(mpls_ap_pkts);

        return outs;
    }

    public static FWDAPSet separateNonMPLS(FWDAPSet in_pkts)
    {
        FWDAPSet outs = new FWDAPSet(in_pkts);
        outs.intersect(nonmpls_ap_pkts);

        return outs;
    }

    public static void set_MPLS_ap_pkts(APComputer apc)
    {
        mpls_ap_pkts = baw.get_mpls_pkts_ap(apc);
        nonmpls_ap_pkts = baw.get_nonmpls_pkts_ap(apc);
    }

    public HashMap <String, Integer> get_fwbdds_map ()
    {
        return fwbdds;
    }

    long nat_addr;
    int nat_subnet_id = 0; 

    public boolean has_valid_nataddr()
    {
        return nat_addr > 0;
    }

    public boolean find_nat_subnet()
    {
        for(ForwardingRule one_r : fws)
        {
            if(one_r.getprefixlen() < 32)
            {
                nat_addr = one_r.getdestip();
                return true;
            }
        }
        return false;
    }

    public long get_tunnel_exit_addr()
    {
        long exit_addr =  nat_addr + nat_subnet_id;
        nat_subnet_id ++;
        return exit_addr;
        
    }

    /**
     * every time this function is called, 
     * we get a different address 
     * @return
     */
    public long get_tunnelled_pkt()
    {
        long tunnelled_pkt =  nat_addr + nat_subnet_id;
        nat_subnet_id ++;
        
        return tunnelled_pkt;

    }

    public boolean find_nat_subnet(String unusedport)
    {
        for(ForwardingRule one_r : fws)
        {
            if(one_r.getiname().equals(unusedport) && one_r.getprefixlen() < 32)
            {
                nat_addr = one_r.getdestip();
                return true;
            }
        }
        return false;
    }

    /**
     * reuse nat_addr
     * @return
     */
    public long get_mpls_fec()
    {
        long fec = nat_addr + nat_subnet_id;
        nat_subnet_id ++;
        return fec;
    }

    public boolean find_nat_subnet_minlen(String unusedport, int min_len)
    {
        int min_prefixlen = min_len;

        for(ForwardingRule one_r : fws)
        {
            if(one_r.getiname().equals(unusedport) && one_r.getprefixlen() < 32 && one_r.getprefixlen() > 0)
            {
                if(min_prefixlen > one_r.getprefixlen())
                {
                    nat_addr = one_r.getdestip();
                    min_prefixlen = one_r.getprefixlen();
                }
            }
        }
        if(min_prefixlen < min_len)
        {
            return true;
        }
        return false;
    }

    public boolean find_nat_subnet_minlen(String unusedport, int min_len, HashSet<Long> used)
    {
        int min_prefixlen = min_len;
        long offset = 100;

        for(ForwardingRule one_r : fws)
        {
            if(one_r.getiname().equals(unusedport) && one_r.getprefixlen() < 32 && one_r.getprefixlen() > 0 )
            {
                if(min_prefixlen > one_r.getprefixlen())
                {
                    if(!used.contains(one_r.getdestip()))
                    {
                        nat_addr = one_r.getdestip();
                        return true;
                    }else
                    {
                        if(!used.contains(one_r.getdestip()+offset))
                        {
                            nat_addr = one_r.getdestip() + offset;
                            return true;
                        }
                    }

                }
            }
        }
        nat_addr = -1;
        return false;
    }

    public PositionTuple add_nat()
    {
        String port = "nat_port" + nat_subnet_id;
        int nat_addr_bdd = baw.encodeDstIPPrefix(nat_addr+nat_subnet_id, 32);
        
        nat_subnet_id ++;


        fwbdds.put(port, nat_addr_bdd);
        return new PositionTuple(name, port);
    }

    public Device()
    {
        /**
         * do nothing
         */
    }

    public Device(String dname)
    {
        this.name = dname;
        fws = new ArrayList<ForwardingRule>();
        fws6 = new ArrayList<ForwardingRule6>();
        mpls_table = null;
    }

    public void read_mpls_table(String filename)
    {
        mpls_table = new MPLSTable();
        mpls_table.read_mpls_table(new File(filename));
    }

    public void ini_mpls_table()
    {
        mpls_table = new MPLSTable();
    }

    public void ini_IPinIP()
    {
        ip_in_ip = new IPinIP();
    }

    public void add_ipinip_encapsulator(ForwardingRule fec, long exit_ipaddr)
    {
        //System.out.println(name);
        //System.out.println(fec);
        //System.out.println(exit_ipaddr);

        int guard_nobit = baw.encodeDstIPPrefix(fec.getdestip(), fec.getprefixlen());
        int guard = baw.set_field_bit(Fields.dst_ip_inner, guard_nobit, false);
        int guard_no_mpls = baw.set_field_bit(Fields.mpls_label, guard, false);
        
        int header = baw.encodeDstIPPrefix(exit_ipaddr, 32);
        ip_in_ip.add_encapsulator(guard_no_mpls, header);

        baw.deref(guard_nobit);
        baw.deref(guard);

    }

    public void add_ipinip_encapsulator_update(ForwardingRule fec, long exit_ipaddr)
    {
        //System.out.println(name);
        //System.out.println(fec);
        //System.out.println(exit_ipaddr);

        int guard_nobit = baw.encodeDstIPPrefix(fec.getdestip(), fec.getprefixlen());
        int guard = baw.set_field_bit(Fields.dst_ip_inner, guard_nobit, false);
        int header = baw.encodeDstIPPrefix(exit_ipaddr, 32);
        ip_in_ip.add_encapsulator_update(guard, header);

        baw.deref(guard_nobit);

    }

    public void add_ipinip_decapsulator(ForwardingRule fec, long exit_ipaddr)
    {
        int guard_nobit = baw.encodeDstIPPrefix(exit_ipaddr, 32);
        int guard = baw.set_field_bit(Fields.dst_ip_inner, guard_nobit, true);
        int guard_no_mpls = baw.set_field_bit(Fields.mpls_label, guard, false);

        int header_filter = baw.encodeDstIPPrefix(fec.getdestip(), fec.getprefixlen());

        ip_in_ip.add_decapsulator(guard_no_mpls, header_filter);

        baw.deref(guard_nobit);
        baw.deref(guard);
    }

    public void add_ipinip_decapsulator_update(ForwardingRule fec, long exit_ipaddr)
    {
        int guard_nobit = baw.encodeDstIPPrefix(exit_ipaddr, 32);
        int guard = baw.set_field_bit(Fields.dst_ip_inner, guard_nobit, true);

        int header_filter = baw.encodeDstIPPrefix(fec.getdestip(), fec.getprefixlen());

        ip_in_ip.add_decapsulator_update(guard, header_filter);

        baw.deref(guard_nobit);


    }

    public void add_mpls_switch_entry(int in_label, int out_label, HashSet<String> ports)
    {
        mpls_table.add_swap_entry(in_label, out_label, ports);
    }

    public void add_mpls_switch_entry_bdd(int in_label, int out_label, HashSet<String> ports)
    {
        mpls_table.add_swap_entry_bdd(in_label, out_label, ports);
    }

    public void add_mpls_encapsulation_entry(ForwardingRule fec, int out_label, HashSet<String> ports)
    {
        mpls_table.add_entrance_entry(fec, out_label, ports);
    }

    public void add_mpls_encapsulation_entry_bdd(ForwardingRule fec, int out_label, HashSet<String> ports)
    {
        mpls_table.add_entrance_entry_bdd(fec, out_label, ports);
    }

    public void show_fwd_bddsize()
    {
        System.out.println(name);
        int total_size = 0;
        for(Integer one_p : fwbdds.values())
        {
            total_size = total_size + baw.getNodeSize(one_p);
        }
        System.out.println(total_size);
    }

    public HashMap<String, Integer> ForwardAction6(String port, int fwdp)
    {
        HashMap <String, Integer> fwded = new HashMap<String, Integer>();
        if(fwdp == BDDACLWrapper.BDDFalse)
        {
            return fwded;
        }

        Iterator iter = fwbdds6.entrySet().iterator();

        BDD thebdd = baw.getBDD();

        while(iter.hasNext())
        {
            Map.Entry entry = (Map.Entry) iter.next();
            String otherport = (String) entry.getKey();
            //
            //if(!otherport.equals(port))
            {
                int fwtmp1 = thebdd.and(fwdp, (Integer) entry.getValue());

                if(fwtmp1 != BDDACLWrapper.BDDFalse)
                {
                    thebdd.ref(fwtmp1);
                    fwded.put(otherport, fwtmp1);					
                }
            }
        }

        return fwded;
    }

    private HashMap<String, Integer> MPLSForward(String port, int fwdp)
    {
        return mpls_table.ForwardAction(fwdp);
    }

    private HashMap<String, Integer> MPLSEncapsulation(String port, int fwdp)
    {
        return mpls_table.EncapsulateAction(fwdp);
    }

    private HashMap<String, Integer> IPForward(String port, int fwdp)
    {

        HashMap<String, Integer> fwded = new HashMap<String, Integer> ();

        Iterator iter = fwbdds.entrySet().iterator();

        BDD thebdd = baw.getBDD();

        while(iter.hasNext())
        {
            Map.Entry entry = (Map.Entry) iter.next();
            String otherport = (String) entry.getKey();
            //
            //if(!otherport.equals(port))
            {
                int fwtmp1 = thebdd.and(fwdp, (Integer) entry.getValue());

                if(fwtmp1 != BDDACLWrapper.BDDFalse)
                {
                    thebdd.ref(fwtmp1);
                    fwded.put(otherport, fwtmp1);					
                }
            }
        }

        return fwded;
    }

    private HashMap<String, Integer> merge_tables_bdd(HashMap<String, Integer> table1,
            HashMap<String, Integer> table2)
            {
        HashMap<String, Integer> merged = new HashMap<String, Integer> (table1);

        BDD thebdd = baw.getBDD();

        for(String port : table2.keySet())
        {
            if(merged.containsKey(port))
            {
                int oldkey = merged.get(port);
                merged.put(port, thebdd.ref(thebdd.or(oldkey, table2.get(port))));
            }else
            {
                merged.put(port, table2.get(port));
            }
        }

        return merged;
            }

    /**
     * 
     * @param table - merged to this table
     * @param table_add -  table to be added
     */
    private static void merge_tables(HashMap<String, FWDAPSet> table, HashMap<String, FWDAPSet> table_add)
    {
        for(String port : table_add.keySet())
        {
            if(table.containsKey(port))
            {
                table.get(port).union(table_add.get(port));
            }else
            {
                table.put(port, table_add.get(port));
            }
        }
    }

    /**
     * 
     * @param port
     * @param pkt set represented by bdd
     * @return <portname, bdd node>
     */
    public HashMap <String, Integer> ForwardAction(String port, int fwdp_raw)
    {
        if(only_v6)
        {
            return ForwardAction6(port, fwdp_raw);
        }

        if(mpls_table != null)
        {    

            int mpls_pkts = baw.separateMPLS(fwdp_raw);
            HashMap<String, Integer> fwded_mpls = MPLSForward(port, mpls_pkts);

            BDD thebdd = baw.getBDD();
            int non_mpls_pkts = baw.separateNonMPLS(fwdp_raw);

            if(fwded_mpls.containsKey(MPLSTable.recv_port))
            {
                int tmp = thebdd.ref(thebdd.or(non_mpls_pkts, 
                        fwded_mpls.get(MPLSTable.recv_port)));
                thebdd.deref(non_mpls_pkts);
                non_mpls_pkts = tmp;
                fwded_mpls.remove(MPLSTable.recv_port);
            }



            HashMap<String, Integer> fwded_encap = MPLSEncapsulation(port, non_mpls_pkts);

            int res_non_mpls_pkts = baw.diff(non_mpls_pkts, mpls_table.all_encapsulated);

            baw.deref(non_mpls_pkts);

            non_mpls_pkts = res_non_mpls_pkts;

            HashMap<String, Integer> fwded_ip = IPForward(port, non_mpls_pkts);




            thebdd.deref(mpls_pkts);
            thebdd.deref(non_mpls_pkts);

            HashMap<String, Integer> results = merge_tables_bdd(fwded_ip, fwded_mpls);

            if(!fwded_encap.isEmpty())
            {
                results = merge_tables_bdd(results, fwded_encap);
            }

            return results;
        }else if(ip_in_ip != null)
        {

            BDD thebdd = baw.getBDD();

            /*
	                if(name.equals("3741"))
	                  {
	                        System.out.println(name);
	                        System.out.println(ip_in_ip.encapsulator_guard_union);
	                        System.out.println(thebdd.getRef(ip_in_ip.encapsulator_guard_union));
	                  }
             */

            //if(!baw.checkIPTunnelPktCorrectness(fwdp_raw))
            //{
            //      System.err.println("forwarding");
            //      System.exit(-1);
            //}
            /**
             *int tmp1 = ip_in_ip.perform_decapsulation(fwdp_raw);
             */
            //if(!baw.checkIPTunnelPktCorrectness(tmp1))
            //{
            //      System.err.println("decap");
            //      System.exit(-1);   
            //}
            /**
            int tmp2 = ip_in_ip.perform_encapsulation(tmp1);
             */
            int aftertunnel = ip_in_ip.ForwardAction(fwdp_raw);


            /*
                  if(name.equals("3741"))
                  {
                        System.out.println("after encapsulation");
                        System.out.println(ip_in_ip.encapsulator_guard_union);
                        System.out.println(thebdd.getRef(ip_in_ip.encapsulator_guard_union));
                  }*/
            //if(!baw.checkIPTunnelPktCorrectness(tmp2))
            //{
            //     System.err.println("encap");
            //    System.exit(-1);   
            //}

            HashMap<String, Integer> fwded = IPForward(port, aftertunnel);

            thebdd.deref(aftertunnel);
            /**
            thebdd.deref(tmp1);
            thebdd.deref(tmp2);
             */
            return fwded;

        }
        else
        {
            return IPForward(port, fwdp_raw);
        }

    }



    public Collection<Integer> getfwbdds()
    {
        return fwbdds.values();
    }

    public void computeFWBDDs()
    {
        Collections.sort(fws);
        this.fwbdds = Device.baw.getfwdbdds_sorted_no_store(fws);
        //this.fwbdds = Device.baw.getfwdbdds(fws);

        //System.out.println(fwbdds.size());
        //for(String iname : fwbdds.keySet())
        //{
        //	System.out.println(iname + ": " + fwbdds.get(iname));
        //}
    }

    public void computeFWBDDs6()
    {
        this.fwbdds6 = baw.getfwdbdds6(fws6);
    }

    public void addFW(ForwardingRule fw)
    {
        fws.add(fw);
    }

    public void addFW(ForwardingRule6 fw)
    {
        fws6.add(fw);
    }

    private HashMap<String, FWDAPSet> IPForward(String port, FWDAPSet fwdaps)
    {
        HashMap <String, FWDAPSet> fwded = new HashMap<String, FWDAPSet>();


        //System.out.println(fwaps.keySet());
        Iterator iter = fwaps.entrySet().iterator();
        while(iter.hasNext())
        //for(String otherport : fwaps.keySet())
        {
            Map.Entry entry = (Map.Entry) iter.next();
            String otherport = (String) entry.getKey();
            //if(!otherport.equals(port))
            {
                FWDAPSet fwtmp1 = new FWDAPSet(fwdaps);
                fwtmp1.intersect(fwaps.get(otherport));
                if(!fwtmp1.isempty())
                {

                    fwded.put(otherport, fwtmp1);                         

                }
            }
        }

        /**
            Iterator iter = fwaps.entrySet().iterator();
            while(iter.hasNext())
            {
                  Map.Entry entry = (Map.Entry) iter.next();
                  String otherport = (String) entry.getKey();
                  //
                  if(!otherport.equals(port))
                  {
                        FWDAPSet fwtmp1 = new FWDAPSet(fwdaps);
                        fwtmp1.intersect((FWDAPSet) entry.getValue());
                        if(!fwtmp1.isempty())
                        {

                              fwded.put(otherport, fwtmp1);                         

                        }
                  }
            }*/

        return fwded;
    }

    @Override
    public HashMap<String, FWDAPSet> ForwardAction(String port, FWDAPSet fwdaps)
    {
        if(mpls_table != null)
        {
            FWDAPSet mpls_pkts = separateMPLS(fwdaps);
            HashMap<String, FWDAPSet> fwded_mpls = mpls_table.ForwardAction(mpls_pkts);

            FWDAPSet non_mpls_pkts = separateNonMPLS(fwdaps);

            if(fwded_mpls.containsKey(MPLSTable.recv_port))
            {
                FWDAPSet tmp =  fwded_mpls.get(MPLSTable.recv_port);
                non_mpls_pkts.union(tmp);
                fwded_mpls.remove(MPLSTable.recv_port);
            }

            HashMap<String, FWDAPSet> fwded_encap = mpls_table.EncapsulateAction(non_mpls_pkts);

            HashMap<String, FWDAPSet> fwded_ip = IPForward(port, non_mpls_pkts);

            merge_tables(fwded_mpls, fwded_encap);
            merge_tables(fwded_mpls, fwded_ip);

            return fwded_mpls;
        }
        else if(ip_in_ip != null)
        {
            FWDAPSet transformed = ip_in_ip.ForwardAction(fwdaps);
            return IPForward(port, transformed);

        }else
        {
            return IPForward(port, fwdaps);
        }
    }

    @Override
    public void setaps(APComputer apc) {

        fwaps = new HashMap<String, FWDAPSet>();
        setaps_1(fwaps, fwbdds, apc);
    }

    protected void setaps_1(HashMap<String, FWDAPSet> filteraps, HashMap<String, Integer> filterbdds, APComputer apc)
    {
        for(String portname : filterbdds.keySet())
        {
            HashSet<Integer> rawset = apc.getAPExpComputed(filterbdds.get(portname));
            if(rawset == null)
            {
                System.err.println("bdd expression not found!");
                System.exit(1);
            }else
            {
                FWDAPSet faps = new FWDAPSet(rawset);
                filteraps.put(portname, faps);
            }
        }
    }


}
